import re

#regexes
nextToId = re.compile(r"^\s*\w+")
finalMatchedBrackets = re.compile(r"\[.*\]\s*$")
finalHId = re.compile(r"#\w+\s*$")
aggregateEnd = re.compile(r"^\s*[<>]=?\s*\w+|^\s*=\s*\w+")
finalId = re.compile(r"\w+\s*$")

def matchParen(str, pos):
	count = 1
	i = pos+1
	while i < len(str):
		if str[i] == '(':
			count+=1
		elif str[i] == ')':
			count-=1
		#check if matched
		if count == 0:
			return i
		i+=1
	#not matched
	return -1

def getTokenBetween(str, regex, s, e):
	#find last whitespace before pos
	m = regex.search(str[s:e])
	if m:
		return (m.group(0), m.start(0), m.end(0))
	else:
		return (None,None,None)

def nextChar(str, start, char):
	i = start
	while i < len(str):
		if not str[i].isspace():
			if str[i] == char:
				return i
			break
		i+=1
	return -1

def getVars(str):
	return re.findall(r"[A-Z]\w*",str)

def getTerms(str):
	str = str[str.find('(')+1:str.rfind(')')]
	terms = []
	pos = 0
	while pos < len(str):
		(t,s,e) = getTokenBetween(str,nextToId,pos,len(str))
		if t:
			#found var|num|id, is there a '(' next?
			parenpos = nextChar(str, e+pos, '(')
			if parenpos != -1:
				endterm = matchParen(str,parenpos)
				#matched parens
				if endterm != -1:
					terms.append(str[pos+s:endterm+1])
					pos = endterm+1
				else:
					#unmatched
					raise Exception('Unmateched')
			#no parentheses?
			else:
				terms.append(t)
				pos += e
		#no term could be created
		else:
			raise Exception('Syntax error')
		#check if continuation is possible
		comma = nextChar(str, pos, ',')
		if comma != -1:
			pos = comma+1
			continue
		else:
			break
	#check if there are no garbage chars
	if len(str[pos:].strip()) != 0:
		raise Exception('Syntax error')
	else:
		return terms

#returns table of constructs: <type, id, string>
#types 0->unknown, 1->quantifier, 2->aggregate, 3->atom
def getParams(str, atoms_only):
	pos = 0
	params = []
	while pos < len(str):
		#find a paren
		start = pos
		#find paren, ignoring brackets
		rbrack = str.find(']',start)
		if rbrack != -1:
			pos = str.find('(',rbrack)
		else:
			pos = str.find('(',start)
		if pos == -1:
			#no more specialties
			params.append((0,None,str[start:]))
			break
		else:	
			#match the parens
			end = matchParen(str,pos)
			if end == -1:
				#unmatched parens
				raise Exception('Unmatched parentheses')
			else:
				#find atoms, etc
				if not atoms_only:
					#potential quantifier
					(bracks,p_bracks,e) = getTokenBetween(str, finalMatchedBrackets, start, pos)
					if bracks:
						(t,p,e) = getTokenBetween(str, finalHId, start, p_bracks)
						if t:
							#add
							unk = str[start:p+start]
							if len(unk) != 0:
								params.append((0,None,unk))
							#append quantifier
							params.append((1, t, t+bracks+str[pos:end+1]))
							pos = end+1
							continue
						else:
							raise Exception('Syntax error')
					#potential aggregate
					(agg,agg_p,agg_e) = getTokenBetween(str, finalHId, start, pos)
					if agg:
						#find operators
						(ops, ops_p, ops_e) = getTokenBetween(str,aggregateEnd,end+1,len(str))
						if not ops:
							raise Exception('Syntax error')
						ops_e = ops_e+end
						#add 'unknown' before aggregate
						unk = str[start:agg_p+start]
						if len(unk) != 0:
							params.append((0,None,unk))
						params.append((2, agg, agg+str[pos:ops_e+1]))
						pos = ops_e+1
						continue
				#potential atom
				#get tokens before start
				(atom,atom_p,e) = getTokenBetween(str, finalId, start, pos)
				if atom:
					#add 'unknown' before predicate
					unk = str[start:atom_p+start]
					if len(unk) != 0:
						params.append((0,None,unk))
					#found predicate
					params.append((3, atom, atom+str[pos:end+1]))
					pos = end+1
				#malformed construct
				else:
					raise Exception('Syntax error')
		#param added
	#endwhile
	#check for orphan parens
	for pa in params:
		if pa[0] == 0 and ')' in pa[2]:
			raise Exception('Unmatched parentheses')
	return params

#checks if str is of the form <id>
def getPredicate(str):
	str = str.strip()
	sorts = []
	match = nextToId.search(str)
	if not match:
		raise Exception('Syntax error')
	predicate = match.group(0)
	pos = match.end(0)
	pos = nextChar(str, pos, '(')
	if pos != -1:
		pos+=1
		while True:
			#find sort name
			(n,s,e) = getTokenBetween(str, nextToId, pos, len(str))
			if n:
				#found sort
				sorts.append(n.strip())
				pos += e
			else:
				raise Exception('Syntax error')
			#continue?
			c = nextChar(str, pos, ',')
			if c == -1:
				break
			else:
				pos = c+1
		#check for final )
		if nextChar(str, pos, ')') == len(str)-1:
			#syntax is correct
			return (predicate, sorts)
	#else
	raise Exception('Syntax error')

#NOTES: check orphan parentheses in unknowns